A:Type, F:(Aprop{i:l}), L:(A List).
(k:A. decidable(F(k)))  decidable(l_exists(L; A; k.F(k))) 

latex

Definitions	t  T, x(s), P  Q, prop{i:l}, x:A. B(x), x. t(x), P  Q, P  Q, P  Q, P  Q
Lemmas	decidable wf, decidable false, l exists nil, false wf, l exists wf, decidable functionality, l exists cons, decidable or